T:Type, P:(TProp), L:T List.
0<||L||
 (x, y:T. Dec(x = y))
 ((xL. yL. x = y  T  P(x)  P(y))  (xL.yL. x = y  T  P(y))) 

latex

Definitions	P  Q, P & Q, P  Q, P  Q, False, (xL.P(x)), xL. P(x), x. t(x), A, x(s), Dec(P), P  Q, Prop, ||as||, x:A. B(x), t  T, {T}, ij, (x  l), x:A. B(x), {i..j}, i  j < k, AB, l[i], ij, i<j, hd(l)
Lemmas	exists functionality wrt iff, le wf, select member, cons member, l member wf, all functionality wrt iff, non neg length, l all nil, false wf, iff wf, l exists nil, or functionality wrt iff, iff functionality wrt iff, implies functionality wrt iff, l all cons, and functionality wrt iff, iff transitivity, l exists cons, length wf1, decidable wf, not wf, l all wf, l exists wf